\begin{tabbing}
$\forall$$m$:$\mathbb{N}$, $P$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$$\rightarrow$Prop).
\\[0ex]($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$. Dec($P$($i$)))
\\[0ex]$\Rightarrow$ (\=$\exists$$n$, $k$:$\mathbb{N}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$), $g$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$).\+
\\[0ex]increasing($f$;$n$)
\\[0ex]\& increasing($g$;$k$)
\\[0ex]\& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$. $P$($f$($i$)))
\\[0ex]\& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $\neg$$P$($g$($j$)))
\\[0ex]\& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$. ($\exists$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$. $i$ $=$ $f$($j$) $\in$ $\mathbb{Z}$) $\vee$ ($\exists$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $i$ $=$ $g$($j$) $\in$ $\mathbb{Z}$)))
\-
\end{tabbing}